#include <stdio.h>
#include <time.h> 
#include <iostream>
#include <iomanip>
#include <fstream>
#include <iosfwd>
#include <sstream>
#include <signal.h>
#include <unistd.h>
#include <algorithm>
#include "ToolConfig.hh"
#include "ReadCNF.hh"
#include "auxiliary.hh"
#include "BackboneInformation.hh"
#include "Worker.hh"
#include "LitBitSet.hh"
#include "UpperBound.hh"
#include "CoreBased.hh"
#include "UpperBoundProg.hh"

using std::cout;
using std::cin;
using std::vector;
using std::setprecision;
using namespace minibones;

bool            print_help=false; 
ofstream        output_file;
ToolConfig      config;
Worker          *pworker=NULL;
UpperBound      *pupperbound=NULL;
CoreBased       *pcorebased=NULL;
CoreBased       *scorebased=NULL;
UpperBoundProg  *pupperbound_prog=NULL;
Range           range;
bool            instance_sat = false;

vector<Lit> previous_backbone;
vector<Lit> lresult;


void remove_clauses(CNF & clauses,int length);
void delete_conflict(CNF & clauses,vector<Lit> lresult);
void print_usage();
void print_header();
void print_header(ToolConfig& config);
bool parse_options(int argc, char** argv, /*out*/ToolConfig& config);
bool is_inresult(Lit lit ,  vector<Lit> lresult);
void cnf_cut(CNF clauses,int block_type, CNF & clauses_one, CNF& clauses_two);
vector<Lit> print_backbone(const BackboneInformation& worker, const Range& range, ToolConfig& config, ostream& output);
int  run_worker(ToolConfig& config, ostream& output);
int run_upper_bound(ToolConfig& config, ostream& output);
int run_core_based(ToolConfig& config, ostream& output);
int run_upper_bound_prog(ToolConfig& config, ostream& output);
void register_sig_handlers();
void initialize_picosat();
vector<Lit> run_corebased(ToolConfig& config,ostream& output,CoreBased *pcorebased,Reader* fr);
int main(int argc, char** argv) {
  print_header();
  register_sig_handlers();
  if (!parse_options(argc, argv, config) || print_help) {
     print_usage();
     return -1;
  }

  print_header(config);
  ostream& output=std::cout;
  int return_value;
  if (config.get_self_test()) {
    cout << "running self test" << endl;
    const bool tests_okay =  true;// test_all();
    cout << "self test: " << (tests_okay ? "OK" : "FAIL") << endl;
    return_value = tests_okay ? 0 : 20;
  } else if (config.get_use_upper_bound()) {
    return_value = run_upper_bound(config, output);
  } else if (config.get_use_core_based()) {
    return_value = run_core_based(config, output);
  } else if (config.get_use_upper_bound_prog()) {
    return_value = run_upper_bound_prog(config, output);
  } else {
    return_value = run_worker(config, output);
  }
  if (return_value==10||return_value==20) 
    cout << "i complete" << endl;
  return return_value;
}

Reader* make_reader(string flafile) {
  gzFile ff=Z_NULL;
  if (flafile.size()==1 && flafile[0]=='-') {
    return new Reader(std::cin);
  } else {
    ff = gzopen(flafile.c_str(), "rb");
    if (ff==Z_NULL) {
      cerr << "Unable to open file: " << flafile << endl;
      exit(100);
    }
    return new Reader(ff);
  }
  assert(0);
  return NULL;
}

int run_upper_bound(ToolConfig& config, ostream& output) {
  //read input
  Reader* fr = make_reader(config.get_input_file_name());  
  ReadCNF reader(*fr);
  reader.read();

  //determine which part of variables to compute backbone of
  range=Range(1,reader.get_max_id());
  output << "c range: "<<range.first<<"-"<<range.second<<endl;
  pupperbound = new UpperBound(config,output, reader.get_max_id(), reader.get_clause_vector());
  UpperBound& upperbound=*pupperbound;
  if (!upperbound.initialize()) {//unsatisfiable
    config.prefix(output) << "instance unsatisfiable" << endl;
    output << "s 0" << endl;
    delete pupperbound; 
    return 20;
  }
  instance_sat = true;
  //run upperbound
  upperbound.run();
  config.prefix(output) << "computation completed " << endl;
  cout << "i sc:" << upperbound.get_solver_calls() << endl;
  cout << "i st:" << upperbound.get_solver_time() << endl;
  cout << "i ast:" << setprecision(2) << (upperbound.get_solver_time()/(double)upperbound.get_solver_calls()) << endl;
  //print results
  print_backbone(upperbound, range, config, output);
  delete pupperbound; 
  delete fr;
  return 10;
}


int run_core_based(ToolConfig& config, ostream& output) {
  //block_type  is the type of  creating CNF
   int length,cut_length,i,block_type = 1;
  CNF clauses_next,clauses,clauses_first ;  
  vector<Lit> fresult,sresult ;
  //read input
  Reader* fr = make_reader(config.get_input_file_name());
  ReadCNF reader(*fr);
  try {
    reader.read();
  } catch (const ReadCNFException& e) {
    cerr<<"ERROR while reading: "<<e.what()<<"."<<endl;
    return 100;
  }
  //determine which part of variables to compute backbone of
  range=Range(1,reader.get_max_id());
  output << "c range: "<<range.first<<"-"<<range.second<<endl;
   length = reader.size() ;
   clauses  = reader.get_clause();
   srand((unsigned)time(NULL)); 
   switch(block_type){
                case 0:
                        pcorebased = new CoreBased(config, output, reader.get_max_id(), reader.get_clause_vector());
                        break;
                case 1: 
                        // cut_length = length / 2;
                        cut_length =  20 ;
                        cout<<"length is :"<<length<<"   "<<"the first length is :"<<cut_length<<endl;
                        for(i = 0 ;i < length; ++i){
                             if(i < cut_length) {
                                  clauses_first.push_back(clauses[i]);
                                  // cout<<clauses_first[i]<<endl;
                             }else{
                                  clauses_next.push_back(clauses[i]);
                             }  
                        }
                        pcorebased= new CoreBased(config, output, reader.get_max_id(), clauses_first);
                        scorebased= new CoreBased(config, output, reader.get_max_id(), clauses_next);
                        break;
                case 2:
                         cut_length =  rand()%length+1;
                         cout<<"result---->"<<cut_length<<"   "<<length<<endl;
                          for(i=0 ;i< length;++i){
                             if(i< cut_length) {
                                  clauses_first.push_back(clauses[i]);
                                  // cout<<clauses_first[i]<<endl;
                             }else{
                                 clauses_next.push_back(clauses[i]);
                             }
                        }
                         pcorebased= new CoreBased(config, output, reader.get_max_id(), clauses_first);
                         scorebased= new CoreBased(config, output, reader.get_max_id(), clauses_next);
                         break;                        
   }
    fresult =  run_corebased(config,output,pcorebased,fr);
   if(scorebased != NULL)    {
      sresult = run_corebased(config,output,scorebased,fr);
   }
   delete fr;

   //确定clauses_next,clauses_frist
    
   if(fresult.size() != 0 || sresult.size() != 0)     fresult  =  (fresult.size() == 0)?sresult:fresult;
   int number;
   const int clauses_next_length = clauses_next.size();
   // int cmp_length = clauses_first.size();
   CNF clauses_one, clauses_two;
   int add_length;
   cnf_cut(clauses_first, 0 , clauses_one, clauses_two);
    do{
        number  =  fresult.size() ;
        delete_conflict(clauses_two,fresult);
         cout<<" "<<endl;
        cout<<"删除后:"<<clauses_two.size()<<endl;
        if(clauses_two.size() == 0 ){
            cout<<" "<<endl;
            cout<<" 删除后没有数据"<<endl;
            break;
        }
         // 3 添加删除后的数据     (add_length 为删除后的添加长度)
        add_length = clauses_two.size();
        for (int i = 0; i < add_length;++i){
             clauses_next.push_back(clauses_two[i]);
        } 
        pcorebased= new CoreBased(config, output, reader.get_max_id(), clauses_next);
         fresult = run_corebased(config,output,pcorebased,fr);
        if(fresult.size() == 0){
                  // 4 若结果为不可满足则继续二分,添加二分数据(10     10 )
                 //将后半部分移除(define function to insert and delete data to clauses_next)
                 // 二分不成功
                 cnf_cut(clauses_two ,1, clauses_one, clauses_two);
                 remove_clauses(clauses_next , add_length);
                 for (int i = 0; i < clauses_one.size();++i){
                     clauses_next.push_back(clauses_one[i]);
              } 
               pcorebased= new CoreBased(config, output, reader.get_max_id(), clauses_next);
               fresult = run_corebased(config,output,pcorebased,fr);
               if(fresult.size()  == 0){
                   cout<<" "<<endl;
                    cout<<"二分添加第一部分没有结果"<<endl;
                    break;
               }else{
              //       clauses_next.clear();
              //         for (int i = 0; i < clauses_two.size();++i){
              //        clauses_next.push_back(clauses_two[i]);
              // } 
               }
        }else{
              
             // number  =  fresult.size() ;
             //退出循环
              cout<<" "<<endl;
              cout<<"删除后添加可满足"<<endl;
              break;
        }
   }while(fresult.size() != number);

   return 0;
}


// 移除多余的元素达到没有添加clauses_two前的状态
void remove_clauses(CNF & clauses,int length){
      // int remove_length;
      // remove_length =  clauses.size() - length;
      for (int i = 0; i < length ; ++i){
             clauses.pop_back();
      } 
}
//删除冲突
void delete_conflict(CNF & clauses,vector<Lit> lresult){
  int j;
  bool inresult;
  Lit lci;
  int length = clauses.size();
  for(j = 0;j< length;++j){
         inresult  =  false;
         FOR_EACH(ci, clauses[j]) {
                  lci= *ci;
                  inresult =  is_inresult(lci,lresult);
                  if(!inresult)  break;
          }
          //last data in the result,remove the LitSet
          if(inresult){
              cout<<"删除的子句:"<<clauses[j]<<endl;
              clauses.erase(clauses.begin()+j);
              --length;
              --j;
          }
     }
}
 //修改
//cut the cnf and don't know how to store the cuted cnf
void cnf_cut(CNF clauses,int block_type, CNF & clauses_one, CNF& clauses_two){
   int i,cut_length,length = clauses.size();  
   clauses_one.clear();
   clauses_two.clear();
   srand((unsigned)time(NULL)); 
   switch(block_type){
                case 0:
                // 使用指针实现
                        for(i = 0 ;i < length; ++i){
                                  clauses_one.push_back(clauses[i]);
                                  clauses_two.push_back(clauses[i]);
                             }
                        break;
                case 1: 
                        cut_length =  length / 2 ;
                        for(i = 0 ;i < length; ++i){
                             if(i < cut_length) {
                                  clauses_one.push_back(clauses[i]);
                             }else{
                                  clauses_two.push_back(clauses[i]);
                             }  
                        }
                        break;
                case 2:
                         cut_length =  rand()%length+1;
                          for(i=0 ;i< length;++i){
                             if(i< cut_length) {
                                  clauses_one.push_back(clauses[i]);
                             }else{
                                 clauses_two.push_back(clauses[i]);
                             }
                        }
                         break;                        
   }
}
 //修改
bool is_inresult(Lit lit ,  vector<Lit> lresult){
               int  length;
               length =lresult.size();
               // cout<<"lresult  of    get : "<<length<<endl;
               for(int i = 0 ; i <length; ++i){
                        if(var(lresult[i])== var(lit)&& (int)sign(lresult[i]) != (int)sign (lit))   return true;
               }
                return false;
}
vector<Lit>  run_corebased(ToolConfig& config,ostream& output,CoreBased *pcorebased,Reader* fr){
  CoreBased& corebased=*pcorebased;
  vector<Lit> lresult;
  // instance_sat = false;
  if (!corebased.initialize()) {//unsatisfiable
    config.prefix(output) << "instance unsatisfiable" << endl;
    output << "s 0" << endl;
      //或许应该修改
    delete pcorebased; 
    return lresult;
  }
  //haven't change
  instance_sat = true;
  //run corebased
  corebased.run(previous_backbone);
  config.prefix(output) << "computation completed " << endl;
  cout << "i sc:" << corebased.get_solver_calls() << endl;
  cout << "i st:" << corebased.get_solver_time() << endl;
  cout << "i ast:" << setprecision(2) << (corebased.get_solver_time()/(double)corebased.get_solver_calls()) << endl;
  //print results
  lresult = print_backbone(corebased, range, config, output);
   //或许应该修改
  delete pcorebased; 
  return lresult;
}

int run_upper_bound_prog(ToolConfig& config, ostream& output) {
  //read input
  Reader* fr = make_reader(config.get_input_file_name());  
  ReadCNF reader(*fr);
  reader.read();

  //determine which part of variables to compute backbone of
  range=Range(1,reader.get_max_id());
  output << "i range: "<<range.first<<"-"<<range.second<<endl;
  pupperbound_prog = new UpperBoundProg(config, output, reader.get_max_id(), reader.get_clause_vector());
  UpperBoundProg& upperbound_prog=*pupperbound_prog;
  if (!upperbound_prog.initialize()) {//unsatisfiable
    config.prefix(output) << "instance unsatisfiable" << endl;
    output << "s 0" << endl;
    delete pupperbound_prog; 
    return 20;
  }
  instance_sat = true;
  //run upperbound
  upperbound_prog.run();
  config.prefix(output) << "computation completed " << endl;
  cout << "i sc:" << upperbound_prog.get_solver_calls() << endl;
  cout << "i st:" << upperbound_prog.get_solver_time() << endl;
  cout << "i ast:" << setprecision(2) << (upperbound_prog.get_solver_time()/(double)upperbound_prog.get_solver_calls()) << endl;
  //print results
  print_backbone(upperbound_prog, range, config, output);
  delete pupperbound_prog; 
  delete fr;
  return 10;
}

int run_worker(ToolConfig& config, ostream& output) {
  //read input
  Reader* fr = make_reader(config.get_input_file_name());
  ReadCNF reader(*fr);
  try {
    reader.read();
  } catch (const ReadCNFException& e) {
    cerr<<"ERROR while reading: "<<e.what()<<"."<<endl;
    return 100;
  }

  //determine which part of variables to compute backbone of
  range=Range(1,reader.get_max_id());
  output << "c range: "<<range.first<<"-"<<range.second<<endl;
  pworker = new Worker(config,output, reader.get_max_id(), reader.get_clause_vector(), range);
  Worker& worker=*pworker;
  if (!worker.initialize()) {//unsatisfiable
    config.prefix(output) << "instance unsatisfiable" << endl;
    output << "s 0" << endl;
    delete pworker; 
    return 20;
  }
  instance_sat = true;
  //run worker
  worker.run();
  config.prefix(output) << "computation completed " << endl;
  cout << "i sc:" << worker.get_solver_calls() << endl;
  cout << "i st:" << worker.get_solver_time() << endl;
  cout << "i ast:" << setprecision(2) << (worker.get_solver_time()/(double)worker.get_solver_calls()) << endl;
  //print results
  print_backbone(worker, range, config, output);
  delete pworker; 
  return 10;
}

vector<Lit>  print_backbone(const BackboneInformation& worker, const Range& range, ToolConfig& config, ostream& output) {
  vector<Lit> lresult;
  Lit l;
  bool b;
  //remove all  data in vector
  lresult.clear();
  output << "s 1" << endl;
  output << "v ";
  size_t counter = 0;
  for (Var v = range.first; v <= range.second; ++v) {
    if (worker.is_backbone(v)) {
      ++counter;
      output << ' ';
      output << (worker.backbone_sign(v) ? "" : "-") << v;
      //get the result of sat_solver
      b = worker.backbone_sign(v)?false:true;
      l = mkLit(v,b);
      lresult.push_back(l);
    }
  }

  previous_backbone.clear();
  for (int i = 0; i < lresult.size(); ++i)
  {
    previous_backbone.push_back(lresult[i]);
  }
  cout<<" "<<endl;
  cout<<"the v result  size:"<<lresult.size()<<endl;
  output << endl;
  const float percentage = 100.0 * (float)counter / (float)(range.second - range.first + 1);
  config.prefix(output) << "backbone size: "
                        << counter << " "
                        << setprecision(2) << percentage << "% of range"
                        << endl;
  return lresult;
}

//jpms:bc
/*----------------------------------------------------------------------------*\
 * Purpose: Print runtime header when executing DBBones.
\*----------------------------------------------------------------------------*/
//jpms:ec

void print_header(ToolConfig& config) {
  cout_pref<<"contributors: "<<contribs<<endl;
  cout_pref<<"instance: " << config.get_input_file_name()<<endl;
  cout_pref<<endl;
}

 bool parse_options(int argc, char** argv, ToolConfig& config) {
  opterr = 0;
  int c;
  while ((c = getopt(argc, argv, "eobhikmpuc:rl")) != -1) {
    switch (c) {
    case 'h':
      print_help=true;
      break;
    case 'i':
      config.set_backbone_insertion(1);
      break;
    case 'o':
      config.set_use_cores(true);
      break;
    case 'e':
      config.set_use_core_based(true);
      break;
    case 'p':
      config.set_use_upper_bound_prog(true);
      break;
    case 'u':
      config.set_use_upper_bound(true);
      break;
    case 'r':
      config.set_rotatable_pruning(true);
      break;
    case 'b':
      config.set_use_variable_bumping(1);
      break;
    case 'k':
      config.set_use_chunk_keeping(1);
      break;
    case 'm':
      config.set_use_random_chunks(1);
      break;
    case 'c':
      config.set_chunk_size(atoi(optarg));
      break;
    case 'l':
      config.set_scdc_pruning();
      break;
    case '?':
      if (optopt == 'c')
        fprintf (stderr, "Option -%c requires an argument.\n", optopt);
      else if (isprint(optopt)) fprintf (stderr, "Unknown option `-%c'.\n", optopt);
      else fprintf (stderr,"Unknown option character `\\x%x'.\n",optopt);
      return false;
    default:
      return false;
    }
  }

  if (!print_help && (optind >= argc)) {
     cerr << "ERROR: file name expected" << endl;
     return false;
  } else {
    config.set_self_test(false);
    if(!print_help) config.set_input_file_name(argv[optind]);
  }
  return true;
}


//jpms:bc
/*----------------------------------------------------------------------------*\
 * Purpose: Handler for external signals, namely SIGHUP and SIGINT.
\*----------------------------------------------------------------------------*/
//jpms:ec

static void SIG_handler(int signum);
static void finishup();

void register_sig_handlers() {
  signal(SIGHUP,SIG_handler);
  signal(SIGINT,SIG_handler);
  signal(SIGQUIT,SIG_handler);
  signal(SIGTERM,SIG_handler);
  signal(SIGABRT,SIG_handler);
  signal(SIGALRM,SIG_handler);
}

// Generic handler, for all process termination signals that can be caught
static void SIG_handler(int signum) {
  string signame;
  switch (signum) {
    //case 6:  signame = "SIGABRT"; break;
  case 1:  signame = "SIGHUP"; break;
  case 2:  signame = "SIGINT"; break;
  case 3:  signame = "SIGQUIT"; break;
  case 9:  signame = "SIGKILL"; break;
  case 15: signame = "SIGTERM"; break;
  default: cout << "Invalid signal received...\n"; exit(2); break;
  }
  cout << "dbbones received external signal " << signame << ". " << endl;
  cout << "Terminating and printing whatever computed so far." << endl;
  finishup();
}

static void finishup() {
  if (instance_sat) {
    if (pworker) print_backbone (*pworker , range, config, cout);
    if (pupperbound) print_backbone (*pupperbound, range, config, cout);
    if (pupperbound_prog) print_backbone (*pupperbound_prog, range, config, cout);
  } else cout << "s 0" << endl;
  //  if (pworker) delete pworker;
  exit(instance_sat? 10 : 20);
}


void print_header() {
  cerr<<"c minibones, a tool for backbone computation"<<std::endl;
  cerr<<"c (C) 2012,2013 Mikolas Janota, mikolas.janota@gmail.com"<<std::endl;
}

void print_usage() {
  cout << "USAGE"<<"\tminibones <file name>"<<endl;
  cout<<"    -l ... lifting"<<endl;
  cout<<"    -b ... variable activity bumping"<<endl;
  cout<<"    -r ... rotatable variables"<<endl;
  cout<<"    -e ... corE based approach"<<endl;
  cout<<"    -u ... upper bound"<<endl;
  cout<<"    -c S ... chunk of size S (requires -u or -e)"<<endl;
  cout<<"    -m ... rando*m* content of  chunks (requires -u)"<<endl;
  cout<<"    -i ... insertion of the backbone into the formula after it has been found (this is default in lower bound)"<<endl;
  cout<<"    -k ... which *k*eeps a literal in the chunk until it is decided whether it is  a backbone or not (requires -u)."<<endl;
  cout<<"    -p ... programming chunks (one big clause is programmed to represent different chunks)"<<endl;
  cout << "NOTES:"<<endl;
  cout <<"   if filename is '-', instance is read from the standard input" << endl;
}
